(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(assert (forall ((i Real)) (and (>= (div (to_int d) (to_int g)) 0) (xor (>= 0 a) (<= f 0 (mod (to_int j) (to_int i)) 0 k)) (= c 0))))
(assert (= b (mod (to_int e) (to_int h))))
(check-sat)
